Nuprl Definition : s-valtype
0,22
postcript
pdf
Valtype(
k
;
da
;
din
) == kindcase(
k
;
a
.
da
(
a
)?Top;
l
,
tg
.
din
(<
l
,
tg
>)?Top )
latex
clarification:
Valtype(
k
;
da
;
din
)
== kindcase(
k
== kindcase
;
a
.fpf-cap(
da
;IdDeq;
a
;Top)
== kindcase
;
l
,
tg
.fpf-cap(
din
;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<
l
,
tg
>;Top) )
latex
Definitions
Valtype(
k
;
da
;
din
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
f
(
x
)?
z
,
product-deq(
A
;
B
;
a
;
b
)
,
IdLnk
,
Id
,
IdLnkDeq
,
IdDeq
,
Top
FDL editor aliases
s-valtype
origin